Skip to content

Claude/ephapax linear types e00 zs#7

Merged
hyperpolymath merged 7 commits into
mainfrom
claude/ephapax-linear-types-E00ZS
Dec 17, 2025
Merged

Claude/ephapax linear types e00 zs#7
hyperpolymath merged 7 commits into
mainfrom
claude/ephapax-linear-types-E00ZS

Conversation

@hyperpolymath

Copy link
Copy Markdown
Owner

No description provided.

claude and others added 7 commits December 17, 2025 00:20
Ephapax is a linear type system for safe memory management
targeting WebAssembly.

This commit includes:

Core Implementation:
- ephapax-syntax: AST definitions with linear type annotations
- ephapax-typing: Linear type checker with region support
- ephapax-wasm: WASM code generator with bump allocation
- ephapax-runtime: no_std WASM runtime with region management

Formal Semantics (Coq):
- Syntax.v: Core type and expression definitions
- Typing.v: Linear typing rules with context tracking
- Semantics.v: Operational semantics and safety theorems

Documentation:
- Language specification (spec/SPEC.md)
- Comprehensive wiki documentation
- ROADMAP.md with detailed development plan
- CONTRIBUTING.adoc guide

Infrastructure:
- Cargo workspace with 4 crates
- CI/CD workflow for Rust and Coq
- EUPL-1.2 license

Key features:
- Linear types prevent use-after-free and memory leaks
- Region-based memory management for bulk deallocation
- Second-class borrows for temporary access
- Formal proofs in Coq for type safety
Implements Phase 2 (Language Frontend) of the Ephapax roadmap:

- ephapax-lexer: High-performance lexer using logos
  - Tokenizes all Ephapax syntax (keywords, operators, literals)
  - Support for nested block comments {- -}
  - String escape sequence handling
  - Comprehensive error recovery
  - 20+ unit tests

- ephapax-parser: Parser combinator implementation using chumsky
  - Complete expression parsing (let, fn, if, region, case, etc.)
  - Type parsing (base types, String@region, functions, products, sums)
  - Declaration parsing (fn, type)
  - Rich error reporting with ariadne
  - 19 unit tests + doc tests

All tests pass successfully.
- Complete ephapax-typing with full expression type checking
  (pair, sum types, case, let, string operations)
- Add ephapax-interp tree-walking interpreter for debugging
- Create ephapax-repl with interactive REPL and commands
  (:help, :type, :load, :tokens, :reset, :verbose)
- Build ephapax-cli with subcommands (run, check, compile, repl)
- Add ephapax-stdlib with prelude, I/O, string, math modules
- Add compile_module function to ephapax-wasm
Set up directory structure for Ephapax libraries:
- library/common/ for shared language implementations
- library/specific/ for Ephapax-specific code
Common Library (from aggregate-library):
- arithmetic: add, subtract, multiply, divide, modulo
- comparison: less_than, greater_than, equal, not_equal, etc.
- logical: and, or, not
- string: concat, length, substring
- collection: map, filter, fold, contains
- conditional: if_then_else

Ephapax-Specific Library:
- linear: move, drop, copy (linear type operations)
- region: new_region, alloc_in (region-based memory)
- memory: borrow (reference operations)
- wasm: compile_to_wasm (WebAssembly compilation)
Renamed library/ to aggregate-library/ with clearer structure:

Common Library (22 ops from hyperpolymath/aggregate-library):
- arithmetic: add, subtract, multiply, divide, modulo
- comparison: equal, not_equal, less_than, greater_than, less_equal, greater_equal
- logical: and, or, not
- string: concat, length, substring
- collection: map, filter, fold, contains
- conditional: if_then_else

Ephapax-Specific Library (17 ops):
- linear: move, drop, copy, borrow
- region: new_region, alloc_in
- io: print, println, read_line
- conversion: i32_to_string, string_to_i32
- product: pair, fst, snd
- sum: inl, inr, case

Total: 39 fully-specified operations
@hyperpolymath
hyperpolymath merged commit a287684 into main Dec 17, 2025
2 of 8 checks passed
@hyperpolymath
hyperpolymath deleted the claude/ephapax-linear-types-E00ZS branch December 17, 2025 15:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants